R:es_realizer{i:l}. R-Feasible{i:l}(R)  Prop{i'} 

latex

Definitions

Id, t  T, Knd, type List, True, Type, x.A(x), x:A. B(x), IdLnk, x. t(x), a:A fp B(a), x:AB(x), State(ds), f(a), x:AB(x), x:A. B(x), Dec(P), Normal(ds), P & Q, Normal(T), DeclaredType(ds;x), source(l), P  Q, lnk(k), destination(l), s = t, Void, tag(k), IdDeq, f(x)?z, isrcv(k), b, AtomFree(T;x), Realizer, A || B, x,y,z. t(x;y;z), x,y,z,w,v. t(x;y;z;w;v), x,y,z,u,v,w. t(x;y;z;u;v;w), x,y,z,w. t(x;y;z;w), R-Feasible(R), Prop, lexpr{i}

Lemmas

es realizer ind wf, R-compat wf, es realizer wf, atom-free wf, assert wf, isrcv wf, fpf-cap wf, id-deq wf, tagof wf, ldst wf, lnk wf, lsrc wf, decl-type wf, normal-type wf, normal-ds wf, decidable wf, decl-state wf, fpf wf, IdLnk wf, true wf, Knd wf, Id wf